Theory Infinite
theory Infinite imports Main begin class infinite = assumes infinite_UNIV: "infinite (UNIV :: 'a set)" begin lemma arb_element: "finite Y â¹ âx :: 'a. x â Y" using ex_new_if_finite infinite_UNIV by blast lemma arb_finite_subset: "finite Y â¹ âX :: 'a set. Y â© X = {} â§ finite X â§ n ⤠card X" proof - assume fin: "finite Y" then obtain X where "X â UNIV - Y" "finite X" "n ⤠card X" using infinite_UNIV by (metis Compl_eq_Diff_UNIV finite_compl infinite_arbitrarily_large order_refl) then show ?thesis by auto qed lemma arb_countable_map: "finite Y â¹ âf :: (nat â 'a). inj f â§ range f â UNIV - Y" using infinite_UNIV by (auto simp: infinite_countable_subset) end instance nat :: infinite by standard auto end
lass="head">
Theory FO
theory FO imports Main begin abbreviation "sorted_distinct xs â¡ sorted xs â§ distinct xs"